T:Type, L1, L2:T List, x, y:T.
(y  L1)  (y  L2)  x before y  L1 @ L2  x before y  L1 

latex

Definitions	hd(l), i<j, ij, l[i], tl(l), last(L), False, null(as), b, t  T, x:A. B(x), (x  l), A, as @ bs, L1  L2, P  Q, x before y  l
Lemmas	sublist wf, append wf, not wf, l member wf, sublist append front, assert wf, null wf